'Weak Dependency Graph [60.0]'
------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ D(t()) -> 1()
, D(constant()) -> 0()
, D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))
, D(minus(x)) -> minus(D(x))
, D(div(x, y)) -> -(div(D(x), y), div(*(x, D(y)), pow(y, 2())))
, D(ln(x)) -> div(D(x), x)
, D(pow(x, y)) ->
+(*(*(y, pow(x, -(y, 1()))), D(x)), *(*(pow(x, y), ln(x)), D(y)))}
Details:
We have computed the following set of weak (innermost) dependency pairs:
{ D^#(t()) -> c_0()
, D^#(constant()) -> c_1()
, D^#(+(x, y)) -> c_2(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(-(x, y)) -> c_4(D^#(x), D^#(y))
, D^#(minus(x)) -> c_5(D^#(x))
, D^#(div(x, y)) -> c_6(D^#(x), D^#(y))
, D^#(ln(x)) -> c_7(D^#(x))
, D^#(pow(x, y)) -> c_8(D^#(x), D^#(y))}
The usable rules are:
{}
The estimated dependency graph contains the following edges:
{D^#(+(x, y)) -> c_2(D^#(x), D^#(y))}
==> {D^#(pow(x, y)) -> c_8(D^#(x), D^#(y))}
{D^#(+(x, y)) -> c_2(D^#(x), D^#(y))}
==> {D^#(ln(x)) -> c_7(D^#(x))}
{D^#(+(x, y)) -> c_2(D^#(x), D^#(y))}
==> {D^#(div(x, y)) -> c_6(D^#(x), D^#(y))}
{D^#(+(x, y)) -> c_2(D^#(x), D^#(y))}
==> {D^#(minus(x)) -> c_5(D^#(x))}
{D^#(+(x, y)) -> c_2(D^#(x), D^#(y))}
==> {D^#(-(x, y)) -> c_4(D^#(x), D^#(y))}
{D^#(+(x, y)) -> c_2(D^#(x), D^#(y))}
==> {D^#(*(x, y)) -> c_3(D^#(x), D^#(y))}
{D^#(+(x, y)) -> c_2(D^#(x), D^#(y))}
==> {D^#(+(x, y)) -> c_2(D^#(x), D^#(y))}
{D^#(+(x, y)) -> c_2(D^#(x), D^#(y))}
==> {D^#(constant()) -> c_1()}
{D^#(+(x, y)) -> c_2(D^#(x), D^#(y))}
==> {D^#(t()) -> c_0()}
{D^#(*(x, y)) -> c_3(D^#(x), D^#(y))}
==> {D^#(pow(x, y)) -> c_8(D^#(x), D^#(y))}
{D^#(*(x, y)) -> c_3(D^#(x), D^#(y))}
==> {D^#(ln(x)) -> c_7(D^#(x))}
{D^#(*(x, y)) -> c_3(D^#(x), D^#(y))}
==> {D^#(div(x, y)) -> c_6(D^#(x), D^#(y))}
{D^#(*(x, y)) -> c_3(D^#(x), D^#(y))}
==> {D^#(minus(x)) -> c_5(D^#(x))}
{D^#(*(x, y)) -> c_3(D^#(x), D^#(y))}
==> {D^#(-(x, y)) -> c_4(D^#(x), D^#(y))}
{D^#(*(x, y)) -> c_3(D^#(x), D^#(y))}
==> {D^#(*(x, y)) -> c_3(D^#(x), D^#(y))}
{D^#(*(x, y)) -> c_3(D^#(x), D^#(y))}
==> {D^#(+(x, y)) -> c_2(D^#(x), D^#(y))}
{D^#(*(x, y)) -> c_3(D^#(x), D^#(y))}
==> {D^#(constant()) -> c_1()}
{D^#(*(x, y)) -> c_3(D^#(x), D^#(y))}
==> {D^#(t()) -> c_0()}
{D^#(-(x, y)) -> c_4(D^#(x), D^#(y))}
==> {D^#(pow(x, y)) -> c_8(D^#(x), D^#(y))}
{D^#(-(x, y)) -> c_4(D^#(x), D^#(y))}
==> {D^#(ln(x)) -> c_7(D^#(x))}
{D^#(-(x, y)) -> c_4(D^#(x), D^#(y))}
==> {D^#(div(x, y)) -> c_6(D^#(x), D^#(y))}
{D^#(-(x, y)) -> c_4(D^#(x), D^#(y))}
==> {D^#(minus(x)) -> c_5(D^#(x))}
{D^#(-(x, y)) -> c_4(D^#(x), D^#(y))}
==> {D^#(-(x, y)) -> c_4(D^#(x), D^#(y))}
{D^#(-(x, y)) -> c_4(D^#(x), D^#(y))}
==> {D^#(*(x, y)) -> c_3(D^#(x), D^#(y))}
{D^#(-(x, y)) -> c_4(D^#(x), D^#(y))}
==> {D^#(+(x, y)) -> c_2(D^#(x), D^#(y))}
{D^#(-(x, y)) -> c_4(D^#(x), D^#(y))}
==> {D^#(constant()) -> c_1()}
{D^#(-(x, y)) -> c_4(D^#(x), D^#(y))}
==> {D^#(t()) -> c_0()}
{D^#(minus(x)) -> c_5(D^#(x))}
==> {D^#(pow(x, y)) -> c_8(D^#(x), D^#(y))}
{D^#(minus(x)) -> c_5(D^#(x))}
==> {D^#(ln(x)) -> c_7(D^#(x))}
{D^#(minus(x)) -> c_5(D^#(x))}
==> {D^#(div(x, y)) -> c_6(D^#(x), D^#(y))}
{D^#(minus(x)) -> c_5(D^#(x))}
==> {D^#(minus(x)) -> c_5(D^#(x))}
{D^#(minus(x)) -> c_5(D^#(x))}
==> {D^#(-(x, y)) -> c_4(D^#(x), D^#(y))}
{D^#(minus(x)) -> c_5(D^#(x))}
==> {D^#(*(x, y)) -> c_3(D^#(x), D^#(y))}
{D^#(minus(x)) -> c_5(D^#(x))}
==> {D^#(+(x, y)) -> c_2(D^#(x), D^#(y))}
{D^#(minus(x)) -> c_5(D^#(x))}
==> {D^#(constant()) -> c_1()}
{D^#(minus(x)) -> c_5(D^#(x))}
==> {D^#(t()) -> c_0()}
{D^#(div(x, y)) -> c_6(D^#(x), D^#(y))}
==> {D^#(pow(x, y)) -> c_8(D^#(x), D^#(y))}
{D^#(div(x, y)) -> c_6(D^#(x), D^#(y))}
==> {D^#(ln(x)) -> c_7(D^#(x))}
{D^#(div(x, y)) -> c_6(D^#(x), D^#(y))}
==> {D^#(div(x, y)) -> c_6(D^#(x), D^#(y))}
{D^#(div(x, y)) -> c_6(D^#(x), D^#(y))}
==> {D^#(minus(x)) -> c_5(D^#(x))}
{D^#(div(x, y)) -> c_6(D^#(x), D^#(y))}
==> {D^#(-(x, y)) -> c_4(D^#(x), D^#(y))}
{D^#(div(x, y)) -> c_6(D^#(x), D^#(y))}
==> {D^#(*(x, y)) -> c_3(D^#(x), D^#(y))}
{D^#(div(x, y)) -> c_6(D^#(x), D^#(y))}
==> {D^#(+(x, y)) -> c_2(D^#(x), D^#(y))}
{D^#(div(x, y)) -> c_6(D^#(x), D^#(y))}
==> {D^#(constant()) -> c_1()}
{D^#(div(x, y)) -> c_6(D^#(x), D^#(y))}
==> {D^#(t()) -> c_0()}
{D^#(ln(x)) -> c_7(D^#(x))}
==> {D^#(pow(x, y)) -> c_8(D^#(x), D^#(y))}
{D^#(ln(x)) -> c_7(D^#(x))}
==> {D^#(ln(x)) -> c_7(D^#(x))}
{D^#(ln(x)) -> c_7(D^#(x))}
==> {D^#(div(x, y)) -> c_6(D^#(x), D^#(y))}
{D^#(ln(x)) -> c_7(D^#(x))}
==> {D^#(minus(x)) -> c_5(D^#(x))}
{D^#(ln(x)) -> c_7(D^#(x))}
==> {D^#(-(x, y)) -> c_4(D^#(x), D^#(y))}
{D^#(ln(x)) -> c_7(D^#(x))}
==> {D^#(*(x, y)) -> c_3(D^#(x), D^#(y))}
{D^#(ln(x)) -> c_7(D^#(x))}
==> {D^#(+(x, y)) -> c_2(D^#(x), D^#(y))}
{D^#(ln(x)) -> c_7(D^#(x))}
==> {D^#(constant()) -> c_1()}
{D^#(ln(x)) -> c_7(D^#(x))}
==> {D^#(t()) -> c_0()}
{D^#(pow(x, y)) -> c_8(D^#(x), D^#(y))}
==> {D^#(pow(x, y)) -> c_8(D^#(x), D^#(y))}
{D^#(pow(x, y)) -> c_8(D^#(x), D^#(y))}
==> {D^#(ln(x)) -> c_7(D^#(x))}
{D^#(pow(x, y)) -> c_8(D^#(x), D^#(y))}
==> {D^#(div(x, y)) -> c_6(D^#(x), D^#(y))}
{D^#(pow(x, y)) -> c_8(D^#(x), D^#(y))}
==> {D^#(minus(x)) -> c_5(D^#(x))}
{D^#(pow(x, y)) -> c_8(D^#(x), D^#(y))}
==> {D^#(-(x, y)) -> c_4(D^#(x), D^#(y))}
{D^#(pow(x, y)) -> c_8(D^#(x), D^#(y))}
==> {D^#(*(x, y)) -> c_3(D^#(x), D^#(y))}
{D^#(pow(x, y)) -> c_8(D^#(x), D^#(y))}
==> {D^#(+(x, y)) -> c_2(D^#(x), D^#(y))}
{D^#(pow(x, y)) -> c_8(D^#(x), D^#(y))}
==> {D^#(constant()) -> c_1()}
{D^#(pow(x, y)) -> c_8(D^#(x), D^#(y))}
==> {D^#(t()) -> c_0()}
We consider the following path(s):
1) { D^#(+(x, y)) -> c_2(D^#(x), D^#(y))
, D^#(pow(x, y)) -> c_8(D^#(x), D^#(y))
, D^#(ln(x)) -> c_7(D^#(x))
, D^#(div(x, y)) -> c_6(D^#(x), D^#(y))
, D^#(minus(x)) -> c_5(D^#(x))
, D^#(-(x, y)) -> c_4(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_3(D^#(x), D^#(y))}
The usable rules for this path are empty.
We have oriented the usable rules with the following strongly linear interpretation:
Interpretation Functions:
D(x1) = [0] x1 + [0]
t() = [0]
1() = [0]
constant() = [0]
0() = [0]
+(x1, x2) = [0] x1 + [0] x2 + [0]
*(x1, x2) = [0] x1 + [0] x2 + [0]
-(x1, x2) = [0] x1 + [0] x2 + [0]
minus(x1) = [0] x1 + [0]
div(x1, x2) = [0] x1 + [0] x2 + [0]
pow(x1, x2) = [0] x1 + [0] x2 + [0]
2() = [0]
ln(x1) = [0] x1 + [0]
D^#(x1) = [0] x1 + [0]
c_0() = [0]
c_1() = [0]
c_2(x1, x2) = [0] x1 + [0] x2 + [0]
c_3(x1, x2) = [0] x1 + [0] x2 + [0]
c_4(x1, x2) = [0] x1 + [0] x2 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1, x2) = [0] x1 + [0] x2 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1, x2) = [0] x1 + [0] x2 + [0]
We have applied the subprocessor on the resulting DP-problem:
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules:
{ D^#(+(x, y)) -> c_2(D^#(x), D^#(y))
, D^#(pow(x, y)) -> c_8(D^#(x), D^#(y))
, D^#(ln(x)) -> c_7(D^#(x))
, D^#(div(x, y)) -> c_6(D^#(x), D^#(y))
, D^#(minus(x)) -> c_5(D^#(x))
, D^#(-(x, y)) -> c_4(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_3(D^#(x), D^#(y))}
Weak Rules: {}
Details:
We apply the weight gap principle, strictly orienting the rules
{D^#(minus(x)) -> c_5(D^#(x))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{D^#(minus(x)) -> c_5(D^#(x))}
Details:
Interpretation Functions:
D(x1) = [0] x1 + [0]
t() = [0]
1() = [0]
constant() = [0]
0() = [0]
+(x1, x2) = [1] x1 + [1] x2 + [0]
*(x1, x2) = [1] x1 + [1] x2 + [0]
-(x1, x2) = [1] x1 + [1] x2 + [0]
minus(x1) = [1] x1 + [8]
div(x1, x2) = [1] x1 + [1] x2 + [0]
pow(x1, x2) = [1] x1 + [1] x2 + [0]
2() = [0]
ln(x1) = [1] x1 + [0]
D^#(x1) = [1] x1 + [1]
c_0() = [0]
c_1() = [0]
c_2(x1, x2) = [1] x1 + [1] x2 + [1]
c_3(x1, x2) = [1] x1 + [1] x2 + [1]
c_4(x1, x2) = [1] x1 + [1] x2 + [1]
c_5(x1) = [1] x1 + [0]
c_6(x1, x2) = [1] x1 + [1] x2 + [1]
c_7(x1) = [1] x1 + [0]
c_8(x1, x2) = [1] x1 + [1] x2 + [1]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{D^#(*(x, y)) -> c_3(D^#(x), D^#(y))}
and weakly orienting the rules
{D^#(minus(x)) -> c_5(D^#(x))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{D^#(*(x, y)) -> c_3(D^#(x), D^#(y))}
Details:
Interpretation Functions:
D(x1) = [0] x1 + [0]
t() = [0]
1() = [0]
constant() = [0]
0() = [0]
+(x1, x2) = [1] x1 + [1] x2 + [0]
*(x1, x2) = [1] x1 + [1] x2 + [8]
-(x1, x2) = [1] x1 + [1] x2 + [0]
minus(x1) = [1] x1 + [2]
div(x1, x2) = [1] x1 + [1] x2 + [0]
pow(x1, x2) = [1] x1 + [1] x2 + [0]
2() = [0]
ln(x1) = [1] x1 + [0]
D^#(x1) = [1] x1 + [1]
c_0() = [0]
c_1() = [0]
c_2(x1, x2) = [1] x1 + [1] x2 + [1]
c_3(x1, x2) = [1] x1 + [1] x2 + [1]
c_4(x1, x2) = [1] x1 + [1] x2 + [1]
c_5(x1) = [1] x1 + [0]
c_6(x1, x2) = [1] x1 + [1] x2 + [1]
c_7(x1) = [1] x1 + [0]
c_8(x1, x2) = [1] x1 + [1] x2 + [1]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{D^#(div(x, y)) -> c_6(D^#(x), D^#(y))}
and weakly orienting the rules
{ D^#(*(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(minus(x)) -> c_5(D^#(x))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{D^#(div(x, y)) -> c_6(D^#(x), D^#(y))}
Details:
Interpretation Functions:
D(x1) = [0] x1 + [0]
t() = [0]
1() = [0]
constant() = [0]
0() = [0]
+(x1, x2) = [1] x1 + [1] x2 + [0]
*(x1, x2) = [1] x1 + [1] x2 + [8]
-(x1, x2) = [1] x1 + [1] x2 + [0]
minus(x1) = [1] x1 + [0]
div(x1, x2) = [1] x1 + [1] x2 + [8]
pow(x1, x2) = [1] x1 + [1] x2 + [0]
2() = [0]
ln(x1) = [1] x1 + [0]
D^#(x1) = [1] x1 + [1]
c_0() = [0]
c_1() = [0]
c_2(x1, x2) = [1] x1 + [1] x2 + [1]
c_3(x1, x2) = [1] x1 + [1] x2 + [1]
c_4(x1, x2) = [1] x1 + [1] x2 + [1]
c_5(x1) = [1] x1 + [0]
c_6(x1, x2) = [1] x1 + [1] x2 + [1]
c_7(x1) = [1] x1 + [0]
c_8(x1, x2) = [1] x1 + [1] x2 + [1]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{D^#(-(x, y)) -> c_4(D^#(x), D^#(y))}
and weakly orienting the rules
{ D^#(div(x, y)) -> c_6(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(minus(x)) -> c_5(D^#(x))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{D^#(-(x, y)) -> c_4(D^#(x), D^#(y))}
Details:
Interpretation Functions:
D(x1) = [0] x1 + [0]
t() = [0]
1() = [0]
constant() = [0]
0() = [0]
+(x1, x2) = [1] x1 + [1] x2 + [0]
*(x1, x2) = [1] x1 + [1] x2 + [8]
-(x1, x2) = [1] x1 + [1] x2 + [8]
minus(x1) = [1] x1 + [0]
div(x1, x2) = [1] x1 + [1] x2 + [7]
pow(x1, x2) = [1] x1 + [1] x2 + [0]
2() = [0]
ln(x1) = [1] x1 + [0]
D^#(x1) = [1] x1 + [1]
c_0() = [0]
c_1() = [0]
c_2(x1, x2) = [1] x1 + [1] x2 + [1]
c_3(x1, x2) = [1] x1 + [1] x2 + [1]
c_4(x1, x2) = [1] x1 + [1] x2 + [1]
c_5(x1) = [1] x1 + [0]
c_6(x1, x2) = [1] x1 + [1] x2 + [1]
c_7(x1) = [1] x1 + [0]
c_8(x1, x2) = [1] x1 + [1] x2 + [1]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{D^#(ln(x)) -> c_7(D^#(x))}
and weakly orienting the rules
{ D^#(-(x, y)) -> c_4(D^#(x), D^#(y))
, D^#(div(x, y)) -> c_6(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(minus(x)) -> c_5(D^#(x))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{D^#(ln(x)) -> c_7(D^#(x))}
Details:
Interpretation Functions:
D(x1) = [0] x1 + [0]
t() = [0]
1() = [0]
constant() = [0]
0() = [0]
+(x1, x2) = [1] x1 + [1] x2 + [0]
*(x1, x2) = [1] x1 + [1] x2 + [7]
-(x1, x2) = [1] x1 + [1] x2 + [8]
minus(x1) = [1] x1 + [15]
div(x1, x2) = [1] x1 + [1] x2 + [8]
pow(x1, x2) = [1] x1 + [1] x2 + [0]
2() = [0]
ln(x1) = [1] x1 + [8]
D^#(x1) = [1] x1 + [1]
c_0() = [0]
c_1() = [0]
c_2(x1, x2) = [1] x1 + [1] x2 + [1]
c_3(x1, x2) = [1] x1 + [1] x2 + [1]
c_4(x1, x2) = [1] x1 + [1] x2 + [1]
c_5(x1) = [1] x1 + [15]
c_6(x1, x2) = [1] x1 + [1] x2 + [1]
c_7(x1) = [1] x1 + [7]
c_8(x1, x2) = [1] x1 + [1] x2 + [1]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{D^#(pow(x, y)) -> c_8(D^#(x), D^#(y))}
and weakly orienting the rules
{ D^#(ln(x)) -> c_7(D^#(x))
, D^#(-(x, y)) -> c_4(D^#(x), D^#(y))
, D^#(div(x, y)) -> c_6(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(minus(x)) -> c_5(D^#(x))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{D^#(pow(x, y)) -> c_8(D^#(x), D^#(y))}
Details:
Interpretation Functions:
D(x1) = [0] x1 + [0]
t() = [0]
1() = [0]
constant() = [0]
0() = [0]
+(x1, x2) = [1] x1 + [1] x2 + [0]
*(x1, x2) = [1] x1 + [1] x2 + [8]
-(x1, x2) = [1] x1 + [1] x2 + [2]
minus(x1) = [1] x1 + [7]
div(x1, x2) = [1] x1 + [1] x2 + [8]
pow(x1, x2) = [1] x1 + [1] x2 + [8]
2() = [0]
ln(x1) = [1] x1 + [0]
D^#(x1) = [1] x1 + [1]
c_0() = [0]
c_1() = [0]
c_2(x1, x2) = [1] x1 + [1] x2 + [1]
c_3(x1, x2) = [1] x1 + [1] x2 + [3]
c_4(x1, x2) = [1] x1 + [1] x2 + [1]
c_5(x1) = [1] x1 + [1]
c_6(x1, x2) = [1] x1 + [1] x2 + [3]
c_7(x1) = [1] x1 + [0]
c_8(x1, x2) = [1] x1 + [1] x2 + [6]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{D^#(+(x, y)) -> c_2(D^#(x), D^#(y))}
and weakly orienting the rules
{ D^#(pow(x, y)) -> c_8(D^#(x), D^#(y))
, D^#(ln(x)) -> c_7(D^#(x))
, D^#(-(x, y)) -> c_4(D^#(x), D^#(y))
, D^#(div(x, y)) -> c_6(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(minus(x)) -> c_5(D^#(x))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{D^#(+(x, y)) -> c_2(D^#(x), D^#(y))}
Details:
Interpretation Functions:
D(x1) = [0] x1 + [0]
t() = [0]
1() = [0]
constant() = [0]
0() = [0]
+(x1, x2) = [1] x1 + [1] x2 + [8]
*(x1, x2) = [1] x1 + [1] x2 + [8]
-(x1, x2) = [1] x1 + [1] x2 + [2]
minus(x1) = [1] x1 + [1]
div(x1, x2) = [1] x1 + [1] x2 + [8]
pow(x1, x2) = [1] x1 + [1] x2 + [8]
2() = [0]
ln(x1) = [1] x1 + [0]
D^#(x1) = [1] x1 + [1]
c_0() = [0]
c_1() = [0]
c_2(x1, x2) = [1] x1 + [1] x2 + [1]
c_3(x1, x2) = [1] x1 + [1] x2 + [1]
c_4(x1, x2) = [1] x1 + [1] x2 + [1]
c_5(x1) = [1] x1 + [0]
c_6(x1, x2) = [1] x1 + [1] x2 + [6]
c_7(x1) = [1] x1 + [0]
c_8(x1, x2) = [1] x1 + [1] x2 + [7]
Finally we apply the subprocessor
'Empty TRS'
-----------
Answer: YES(?,O(1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {}
Weak Rules:
{ D^#(+(x, y)) -> c_2(D^#(x), D^#(y))
, D^#(pow(x, y)) -> c_8(D^#(x), D^#(y))
, D^#(ln(x)) -> c_7(D^#(x))
, D^#(-(x, y)) -> c_4(D^#(x), D^#(y))
, D^#(div(x, y)) -> c_6(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(minus(x)) -> c_5(D^#(x))}
Details:
The given problem does not contain any strict rules
2) { D^#(+(x, y)) -> c_2(D^#(x), D^#(y))
, D^#(pow(x, y)) -> c_8(D^#(x), D^#(y))
, D^#(ln(x)) -> c_7(D^#(x))
, D^#(div(x, y)) -> c_6(D^#(x), D^#(y))
, D^#(minus(x)) -> c_5(D^#(x))
, D^#(-(x, y)) -> c_4(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(constant()) -> c_1()}
The usable rules for this path are empty.
We have oriented the usable rules with the following strongly linear interpretation:
Interpretation Functions:
D(x1) = [0] x1 + [0]
t() = [0]
1() = [0]
constant() = [0]
0() = [0]
+(x1, x2) = [0] x1 + [0] x2 + [0]
*(x1, x2) = [0] x1 + [0] x2 + [0]
-(x1, x2) = [0] x1 + [0] x2 + [0]
minus(x1) = [0] x1 + [0]
div(x1, x2) = [0] x1 + [0] x2 + [0]
pow(x1, x2) = [0] x1 + [0] x2 + [0]
2() = [0]
ln(x1) = [0] x1 + [0]
D^#(x1) = [0] x1 + [0]
c_0() = [0]
c_1() = [0]
c_2(x1, x2) = [0] x1 + [0] x2 + [0]
c_3(x1, x2) = [0] x1 + [0] x2 + [0]
c_4(x1, x2) = [0] x1 + [0] x2 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1, x2) = [0] x1 + [0] x2 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1, x2) = [0] x1 + [0] x2 + [0]
We have applied the subprocessor on the resulting DP-problem:
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {D^#(constant()) -> c_1()}
Weak Rules:
{ D^#(+(x, y)) -> c_2(D^#(x), D^#(y))
, D^#(pow(x, y)) -> c_8(D^#(x), D^#(y))
, D^#(ln(x)) -> c_7(D^#(x))
, D^#(div(x, y)) -> c_6(D^#(x), D^#(y))
, D^#(minus(x)) -> c_5(D^#(x))
, D^#(-(x, y)) -> c_4(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_3(D^#(x), D^#(y))}
Details:
We apply the weight gap principle, strictly orienting the rules
{D^#(constant()) -> c_1()}
and weakly orienting the rules
{ D^#(+(x, y)) -> c_2(D^#(x), D^#(y))
, D^#(pow(x, y)) -> c_8(D^#(x), D^#(y))
, D^#(ln(x)) -> c_7(D^#(x))
, D^#(div(x, y)) -> c_6(D^#(x), D^#(y))
, D^#(minus(x)) -> c_5(D^#(x))
, D^#(-(x, y)) -> c_4(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_3(D^#(x), D^#(y))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{D^#(constant()) -> c_1()}
Details:
Interpretation Functions:
D(x1) = [0] x1 + [0]
t() = [0]
1() = [0]
constant() = [0]
0() = [0]
+(x1, x2) = [1] x1 + [1] x2 + [8]
*(x1, x2) = [1] x1 + [1] x2 + [8]
-(x1, x2) = [1] x1 + [1] x2 + [7]
minus(x1) = [1] x1 + [0]
div(x1, x2) = [1] x1 + [1] x2 + [8]
pow(x1, x2) = [1] x1 + [1] x2 + [8]
2() = [0]
ln(x1) = [1] x1 + [15]
D^#(x1) = [1] x1 + [1]
c_0() = [0]
c_1() = [0]
c_2(x1, x2) = [1] x1 + [1] x2 + [3]
c_3(x1, x2) = [1] x1 + [1] x2 + [7]
c_4(x1, x2) = [1] x1 + [1] x2 + [1]
c_5(x1) = [1] x1 + [0]
c_6(x1, x2) = [1] x1 + [1] x2 + [0]
c_7(x1) = [1] x1 + [0]
c_8(x1, x2) = [1] x1 + [1] x2 + [7]
Finally we apply the subprocessor
'Empty TRS'
-----------
Answer: YES(?,O(1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {}
Weak Rules:
{ D^#(constant()) -> c_1()
, D^#(+(x, y)) -> c_2(D^#(x), D^#(y))
, D^#(pow(x, y)) -> c_8(D^#(x), D^#(y))
, D^#(ln(x)) -> c_7(D^#(x))
, D^#(div(x, y)) -> c_6(D^#(x), D^#(y))
, D^#(minus(x)) -> c_5(D^#(x))
, D^#(-(x, y)) -> c_4(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_3(D^#(x), D^#(y))}
Details:
The given problem does not contain any strict rules
3) { D^#(+(x, y)) -> c_2(D^#(x), D^#(y))
, D^#(pow(x, y)) -> c_8(D^#(x), D^#(y))
, D^#(ln(x)) -> c_7(D^#(x))
, D^#(div(x, y)) -> c_6(D^#(x), D^#(y))
, D^#(minus(x)) -> c_5(D^#(x))
, D^#(-(x, y)) -> c_4(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(t()) -> c_0()}
The usable rules for this path are empty.
We have oriented the usable rules with the following strongly linear interpretation:
Interpretation Functions:
D(x1) = [0] x1 + [0]
t() = [0]
1() = [0]
constant() = [0]
0() = [0]
+(x1, x2) = [0] x1 + [0] x2 + [0]
*(x1, x2) = [0] x1 + [0] x2 + [0]
-(x1, x2) = [0] x1 + [0] x2 + [0]
minus(x1) = [0] x1 + [0]
div(x1, x2) = [0] x1 + [0] x2 + [0]
pow(x1, x2) = [0] x1 + [0] x2 + [0]
2() = [0]
ln(x1) = [0] x1 + [0]
D^#(x1) = [0] x1 + [0]
c_0() = [0]
c_1() = [0]
c_2(x1, x2) = [0] x1 + [0] x2 + [0]
c_3(x1, x2) = [0] x1 + [0] x2 + [0]
c_4(x1, x2) = [0] x1 + [0] x2 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1, x2) = [0] x1 + [0] x2 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1, x2) = [0] x1 + [0] x2 + [0]
We have applied the subprocessor on the resulting DP-problem:
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {D^#(t()) -> c_0()}
Weak Rules:
{ D^#(+(x, y)) -> c_2(D^#(x), D^#(y))
, D^#(pow(x, y)) -> c_8(D^#(x), D^#(y))
, D^#(ln(x)) -> c_7(D^#(x))
, D^#(div(x, y)) -> c_6(D^#(x), D^#(y))
, D^#(minus(x)) -> c_5(D^#(x))
, D^#(-(x, y)) -> c_4(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_3(D^#(x), D^#(y))}
Details:
We apply the weight gap principle, strictly orienting the rules
{D^#(t()) -> c_0()}
and weakly orienting the rules
{ D^#(+(x, y)) -> c_2(D^#(x), D^#(y))
, D^#(pow(x, y)) -> c_8(D^#(x), D^#(y))
, D^#(ln(x)) -> c_7(D^#(x))
, D^#(div(x, y)) -> c_6(D^#(x), D^#(y))
, D^#(minus(x)) -> c_5(D^#(x))
, D^#(-(x, y)) -> c_4(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_3(D^#(x), D^#(y))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{D^#(t()) -> c_0()}
Details:
Interpretation Functions:
D(x1) = [0] x1 + [0]
t() = [0]
1() = [0]
constant() = [0]
0() = [0]
+(x1, x2) = [1] x1 + [1] x2 + [8]
*(x1, x2) = [1] x1 + [1] x2 + [8]
-(x1, x2) = [1] x1 + [1] x2 + [7]
minus(x1) = [1] x1 + [0]
div(x1, x2) = [1] x1 + [1] x2 + [8]
pow(x1, x2) = [1] x1 + [1] x2 + [8]
2() = [0]
ln(x1) = [1] x1 + [15]
D^#(x1) = [1] x1 + [1]
c_0() = [0]
c_1() = [0]
c_2(x1, x2) = [1] x1 + [1] x2 + [3]
c_3(x1, x2) = [1] x1 + [1] x2 + [7]
c_4(x1, x2) = [1] x1 + [1] x2 + [1]
c_5(x1) = [1] x1 + [0]
c_6(x1, x2) = [1] x1 + [1] x2 + [0]
c_7(x1) = [1] x1 + [0]
c_8(x1, x2) = [1] x1 + [1] x2 + [7]
Finally we apply the subprocessor
'Empty TRS'
-----------
Answer: YES(?,O(1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {}
Weak Rules:
{ D^#(t()) -> c_0()
, D^#(+(x, y)) -> c_2(D^#(x), D^#(y))
, D^#(pow(x, y)) -> c_8(D^#(x), D^#(y))
, D^#(ln(x)) -> c_7(D^#(x))
, D^#(div(x, y)) -> c_6(D^#(x), D^#(y))
, D^#(minus(x)) -> c_5(D^#(x))
, D^#(-(x, y)) -> c_4(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_3(D^#(x), D^#(y))}
Details:
The given problem does not contain any strict rules